i:Id, ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, ks:Knd List,
tr:(k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)TT).
x  dom(ds)
 (A:Realizer.
 (R-Feasible(A)
 ( R-has-loc(A;i)
 ( (kks. isrcv(k)  R-da(A;source(lnk(k)))(k)?Void  Valtype(da;k))
 ( (kks. k  dom(da))
 ( R-state-var(i;ds;da;x;T;ks;tr) || A) 

latex

Definitions

Id, t  T, Void, x:A. B(x), Top, Type, x.A(x), x:A. B(x), x. t(x), a:A fp B(a), x:AB(x), IdDeq, x : v, f  g, x  dom(f), b, P  Q, False, A, Knd, (x  l), f || g, type List, Valtype(da;k), State(ds), {x:A| B(x) }, Realizer, R-Feasible(R), R-has-loc(R;i), KindDeq, lnk(k), source(l), R-da(R;i), f(x)?z, isrcv(k), Prop, xL. P(x), R-state-var(i;ds;da;x;T;ks;tr), A || B, R-occurs(R;i;z), True, EqDecider(T), P  Q, T, f(a), x(s), x:AB(x), P & Q, P  Q, write-restricted(R;i;k), read-restricted(R; i; y)

Lemmas

read-restricted wf, read-restricted-has-loc, write-restricted wf, write-restricted-has-loc, not-R-has-loc-R-da, fpf-compatible wf, squash wf, true wf, not-R-has-loc-R-ds, subtype rel self, deq wf, fpf-empty-compatible-right, R-occurs wf, R-occurs-has-loc, l all wf, isrcv wf, subtype rel wf, fpf-cap wf, R-da wf, lsrc wf, lnk wf, Kind-deq wf, R-has-loc wf, R-Feasible wf, es realizer wf, not wf, decl-state wf, ma-valtype wf, fpf wf, R-state-var-compat, l member wf, Knd wf, assert wf, fpf-dom wf, fpf-join wf, fpf-single wf, top wf, id-deq wf, fpf-trivial-subtype-top, Id wf